(set-logic QF_UF)
(declare-sort utt$31 0)
(declare-sort utt$32 0)
(declare-fun Concat (Bool utt$31) utt$32)
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)
(declare-fun b4 () Bool)
(declare-fun b5 () Bool)
(declare-fun y0 () utt$31)
(declare-fun y1 () utt$32)
(declare-fun y2 () utt$32)
(declare-fun y3 () utt$32)
(declare-fun y4 () utt$32)

(assert (= b2 (= y1 y3)))
(assert (= y4 (Concat b2 y0)))
(assert (= b3 (= y1 y4)))
(assert (= (not (= y1 y2)) b4))
(assert (not (and b1 b4)))
(assert (= b5 b1))
(assert b5)
(check-sat)
(exit)
